Nuprl Lemma : generated-thread-properties2 11,40

es:ES, P:(E), R:(EE).
single-thread-generator{i:l}(es;P;R)
 (ee':E. (R(e,e'))  (P(e) & P(e')))
 ((ee':E. P(e P(e' (((e R^+ e' (e = e'))  (e' R^+ e)))
 c (xy:E. (P(x) & P(y))  ((R^+(x,y))  (x < y)))
 c (xy:E. (R(x,y))  (R^+!(x,y)))
 c (xyx'y':E. (R^+(x,y))  (R(y',y))  ((R^+(x,y'))  (x = y')))
 c (xyx'y':E. (R^+(x,y))  (R(x',x))  (R(y',y))  (R^+(x',y')))) 
latex


DefinitionsR|P, E <>{TE', x(s), ES, , Type, single-thread-generator{i:l}(es;P;R), A c B, R!, P  Q, (e < e'), P  Q, left + right, s = t, x f y, R^+, x:AB(x), P & Q, x:A  B(x), f(a), E, P  Q, x:AB(x), connex(T;R), Connex(T;x,y.R(x;y)), R^*, {T}, P  Q, xt(x)
Lemmasimplies functionality wrt iff, all functionality wrt iff, rel-star-iff-rel-plus-or, or functionality wrt iff, generated-thread-binrel-properties2

origin